COMMENT ⊗   VALID 00002 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	
 00003 ENDMK
⊗;

CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THM];

EDIT-STRATEGY-IS: 
DEPTH[1]∨LENGTH[5];

ELAPSED-TIME =43351

 
NIL 1 5
1 S(THM2,THM3,THM3,THM1);3 4
3 S(THM3,THM1,THM2,THM3);5 6
4 S(z,u,x,y)⊃S(x,y,z,u);A2
5 S(y,x,z,u)⊃S(x,y,z,u);A3